; COMMAND-LINE: --strings-exp --incremental
(set-logic QF_SLIA)
(declare-const x String)
(declare-const i Int)

(push)
(assert (= i (str.indexof_re (str.++ x "abc") (re.++ re.allchar (str.to_re "b")) 0)))
(assert (= i (str.len x)))
(set-info :status sat)
(check-sat)
(pop)

(push)
(assert (= i (str.indexof_re (str.++ x "abc") (re.++ re.allchar (str.to_re "b")) 0)))
(assert (= i (+ (str.len x) 1)))
(set-info :status unsat)
(check-sat)
(pop)

(push)
(assert (= i (str.indexof_re x (re.++ re.all (str.to_re "a") re.all) 0)))
(assert (= i 0))
(set-info :status sat)
(check-sat)
(pop)

(push)
(assert (= i (str.indexof_re x (re.++ re.all (str.to_re "a") re.all) 0)))
(assert (= i (- 1)))
(set-info :status sat)
(check-sat)
(pop)

(push)
(assert (= 2 (str.indexof_re x (str.to_re "a") 1)))
(set-info :status sat)
(check-sat)
(pop)

(push)
(assert (= i (str.indexof_re x (str.to_re "") 0)))
(assert (= i (str.len x)))
(set-info :status sat)
(check-sat)
(pop)

(push)
(assert (= i (str.indexof_re x (re.comp (str.to_re "")) 0)))
(assert (= i (str.len x)))
(set-info :status unsat)
(check-sat)
(pop)
